x, tg:Id, k:Knd, l:IdLnk, T, A, B:Type, f:(AB(T List)).
((rcv(l,tg) = k)  (T = B))
 ((isrcv(k))  (destination(lnk(k)) = source(l)  Id))
 Normal(A)
 Normal(B)
 Normal(T)
 es.sends1-p(es;x;A;k;B;l;tg;T;f) 

latex

Definitions

R ||- es.P(es), x:A. B(x), T, Y, p q, reduce(f;k;as), f(x), deq-member(eq;x;L), x  dom(f), S  T, Top, f(x)?z, t.2, True, outl(x), t.1, isl(x), , ff, P & Q, tt, if b then t else f fi , x. t(x), x : v, t  T, tag(k), DeclaredType(ds;x), es.P(es), lnk(k), isrcv(k), b, P  Q, x:A. B(x), False, A, P  Q, Unit, , x(s), State(ds), Normal(T), rcv(l,tg), Knd, a = b, locl(a),

Lemmas

sends-p-implies-sends1-p, Knd wf, lsrc wf, lnk wf, ldst wf, isrcv wf, normal-type wf, sends1-p wf, R-realizes wf, event system wf, R-consistent wf, normal-ds-join, normal-ds-single, false wf, not functionality wrt iff, IdLnk wf, true wf, squash wf, rcv wf, assert-eq-id, eq id wf, top wf, fpf-join-cap-sq, fpf-cap-single1, fpf-cap-single-join, subtype rel self, eqof eq btrue, fpf-cap-single, assert of bnot, eqff to assert, not wf, bnot wf, assert wf, iff transitivity, id-deq wf, tagof wf, fpf-single wf3, fpf-join wf, eqtt to assert, bool wf, Id wf, fpf-single wf, sends-p-realizable